module ringElection
open util/ordering[Time] as TO
open util/ordering[Process] as PO

sig Time {}
sig Process {succ: Process, toSend: Process -> Time, elected: set Time}

fact ring {
	all p: Process | Process in p.^succ
	}

pred init (t: Time) {
	all p: Process | p.toSend.t = p
	}

pred step (t, t': Time, p: Process) {
	let from = p.toSend, to = p.succ.toSend |
		some id: from.t {
			from.t' = from.t - id
			-- only accept id if it's greater than my id
			to.t' = to.t + (id - PO/prevs(p.succ))
			}
	}

pred skip (t, t': Time, p: Process) {
	p.toSend.t = p.toSend.t'
	}

fact traces {
	init (TO/first ())
	all t: Time - TO/last() | let t' = TO/next (t) |

		/* simpler form: allows only one process pair to move at a time
		some p: Process |
			step (t, t', p) and all p': Process - (p + p.succ) | skip (t, t', p')
		*/
		all p: Process |
			step (t, t', p) or step (t, t', succ.p) or skip (t, t', p)
	}

-- elected processes is set that received their own id in that step
fact defineElected {
	no elected.TO/first()
	all t: Time - TO/first()|
		elected.t =
			{p: Process | p in p.toSend.t - p.toSend.(TO/prev(t))}
	}

pred show () {
	some elected
	}
run show for 3 but 4 Time

assert AtMostOneElected {
	lone elected.Time
	}
check AtMostOneElected for 5 Process,  10 Time

pred progress () {
	all t: Time - TO/last() |
		let t' = TO/next (t) |
			some Process.toSend.t => some p: Process | not skip (t, t', p)
	}

assert AtLeastOneElected {
	progress () => some t: Time | some elected.t
	}
check AtLeastOneElected for 5 Process, 10 Time

-- compute machine diameter
pred loopless () {
	no disj t, t': Time | toSend.t = toSend.t'
	}
-- diameter is 13 for 3 processes
-- run loopless for 13 Time, 3 Process
run loopless for 33 Time, 5 Process